# Дао функционального программирования

В этом разделе приведены решения упражнений из книги [Бартоша Милевски "Дао функционального программирования"][Дао ФП].

## Упражнение 2.1.1. 

> Предположим, имеются стрелки, \\(f : a \to b\\) и \\(g : b \to c\\). 
> Их композиция \\(g \circ f\\) индуцирует отображение стрелок \\(((g \circ f) \circ -)\\). 
> Покажите, что результат будет таким же, если сначала применить \\((f \circ -)\\), а затем \\((g \circ -)\\). 
> Формально: \\(((g \circ f) \circ -) = (g \circ −) \circ (f \circ −)\\)  
> 
> Подсказка: выберите произвольный объект x и стрелку \\(h : x \to a\\), и посмотрите, получится ли один и тот же результат. 
> Обратите внимание, что \\(\circ\\) здесь перегружен. 
> Это означает регулярную функциональную композицию, когда она помещается между двумя посткомпозициями.

Композиция \\(g \circ f\\) отображает стрелки идущие к a на стрелки идущие к c (\\(g \circ f : a \to b \to c\\)).
\\((f \circ -)\\) отображает стрелки идущие к a на стрелки идущие к b.
\\((g \circ -)\\) отображает стрелки идущие к b на стрелки идущие к c.

Возьмем произвольный объект x и стрелку \\(h : x \to a\\).

Применим \\(((g \circ f) \circ h)\\) к x: \\((g \circ f)(h(x)) = (g \circ f)(a) = c\\).

Применим \\((f \circ -)\\), а затем \\((g \circ -)\\) к x: 
\\(((g \circ −) \circ (f \circ −)(h(x))) = (g \circ −)(f(a)) = g(b) = c\\)

## Упражнение 2.1.2. 

> Проверьте, что композиция из предыдущего упражнения ассоциативна. 
> Подсказка: начните с трех композируемых стрелок.

Предположим, имеются стрелки, \\(f : a \to b\\), \\(g : b \to c\\) и \\(h : c \to d\\).
Докажем, что \\((h \circ g) \circ f = h \circ (g \circ f)\\).
Композиция \\(h \circ g\\) отображает стрелки идущие к b на стрелки идущие к d,
а композиция \\(g \circ f\\) отображает стрелки идущие к a на стрелки идущие к c.

Возьмем произвольный объект x и стрелку \\(j : x \to a\\).

Применим \\((h \circ g) \circ f\\) к x: 
\\(((h \circ g) \circ f)(j(x)) = ((h \circ g)(f(a))) = ((h \circ g)(b)) = d\\).

Применим \\(h \circ (g \circ f)\\) к x:
\\(h \circ (g \circ f)(j(x)) = h \circ (g \circ f)(a) = h(c) = d\\).

Заметим, что ассоциативность композиции одной (строго говоря это не композиция) и двух стрелок очевидна.

Предположим, что доказана ассоциативность композиции n - 1 стрелок, где n > 3. 
Докажем, что композиция n стрелок тоже ассоциативна.

Рассмотрим первую стрелку в композиции - f. 
При расстановке скобок f может применяться либо в последнюю очередь, либо НЕ в последнюю очередь.
Если f применяется в последнюю очередь, то композиция всех предыдущих стрелок является композицией n - 1 стрелок,
а значит - ассоциативна. 
Т.о. не имеет значения в каком порядке мы будем компоновать стрелки, результат всегда будет одинаков. 
Назовем этот результат стрелкой Res.

Если f применяется не в последнюю очередь, а, скажем, в очередь k, где 1 <= k < n, 
то тогда разобьем композицию на три группы: композиция A, состоящая из k - 1 элемента, выполняющаяся в первую очередь,
затем композиция Б, состоящая только из f и композиция В, состоящая из n - k элементов.
Каждая из них ассоциативна, а значит, порядок выполнения стрелок внутри группы не имеет значения.
А значит итоговая композиция равна: \\((В \circ (А \circ Б))\\).
Но эта композиция в точности равна композиции \\(((В \circ А) \circ Б)\\) из-за ассоциативности трех компонуемых стрелок.
Но последняя композиция соответствует одной из композиций, где f применяется в последнюю очередь - т.е. равна Res.

Получается, что композиция n стрелок ассоциативна, потому что все комбинации дают результат Res.

## Упражнение 2.1.3. 

> Покажите, что пред-композиция \\((− \circ f)\\) компонуема, 
> но порядок композиции является обратным: \\((− \circ (g \circ f)) = (− \circ f) \circ (− \circ g)\\)

Если применить \\((− \circ (g \circ f))\\) к стрелкам, исходящим из c, например, к стрелке \\(h : c \to x\\),
направленную в произвольный элемент x, то эта стрелка сопоставляется со стрелкой \\(a \to x\\), 
потому что \\(g \circ f: a \to c\\), но это тоже самое, если вначале применить \\((− \circ g)\\) - 
смещение фокуса с c на b, а затем - \\((− \circ f)\\) - смещение фокуса с b на a.
Получается та же стрелка \\(a \to x\\).

## Упражнение 2.3.1. 

> Что делает \\((id\_{a} \circ −)\\) со стрелками, оканчивающимися на a? 
> Что делает \\((− \circ id\_{a})\\) со стрелками, исходящими из a?

\\((id\_{a} \circ −)\\) оставляет стрелки, оканчивающиеся на a, неизменными. 
Если взять произвольный элемент x и стрелку \\(f : x \to a\\), 
то тогда получим, что \\((id\_{a} \circ f = f)\\).
Аналогично со стрелками, исходящими из a - \\((− \circ id\_{a})\\) оставляет их неизменными.

## Упражнение 3.1.1. 

> Приведите аргумент, что существует биекция между стрелками, исходящими из двух изоморфных объектов. 
> Изобразите соответствующие схемы.

Биекция между исходящими стрелками определяется как \\((- \circ f)\\) или \\((- \circ f^{-1})\\).

## Упражнение 3.1.2. 

> Докажите, что каждый объект изоморфен самому себе.

Тождественная стрелка обратна сама себе, поэтому является изоморфизмом.

## Упражнения 3.1.3-4.

> Если имеются два терминальных объекта, покажите, что они изоморфны.

> Покажите, что изоморфизм из предыдущего упражнения единственен.

Предположим, что \\(i\_{1}\\) и \\(i\_{2}\\) — терминальные объекты в одной и той же категории.
Поскольку \\(i\_{1}\\) терминальный, то существует единственный морфизм **f** от \\(i\_{2}\\) к \\(i\_{1}\\).
Аналогично, поскольку \\(i\_{2}\\) терминальный, то существует единственный морфизм **g** от \\(i\_{1}\\) к \\(i\_{2}\\).
Композиция \\(g \circ f\\) должна быть морфизмом от \\(i\_{2}\\) к \\(i\_{2}\\).
Но \\(i\_{2}\\) является терминальным объектом, так что существует ровно один морфизм от \\(i\_{2}\\) к \\(i\_{2}\\)
и, поскольку начало и конец стрелки совпадают, эта вакансия уже занята тождественным морфизмом.
Следовательно, они должны совпадать: морфизм \\(g \circ f\\) является тождественным.
Аналогично, морфизм \\(f \circ g\\) также совпадает с тождественным,
поскольку может быть всего один морфизм от \\(i\_{1}\\) к \\(i\_{1}\\).
Таким образом, **f** и **g** взаимнообратны, а два терминальных объекта изоморфны.

## Упражнение 3.2.1. 

> Покажите, что обе части условия естественности для \\(f^{−1}\\), при воздействии на h, сводятся к:
> \\(b \overset{f^{-1}}{\rightarrow} a \overset{h}{\rightarrow} x \overset{g}{\rightarrow} y\\)

\\((− \circ f^{−1}) \circ (g \circ −) = f^{−1} \circ g \circ (a \to x) = f^{−1} \circ (a \to y) = b \to y\\)

\\((g \circ −) \circ (− \circ f^{−1}) = (g \circ −) \circ (h \circ f^{−1}) = (g \circ −) \circ (h \circ (b \to a)) = (g \circ −) \circ (b \to x) = b \to y\\)


## Упражнение 3.3.1. 

> Используйте трюк с тождественным морфизмом, чтобы восстановить \\(f^{−1}\\) из семейства отображений \\(\beta\\).

???

## Упражнение 3.3.2. 

> Используя \\(f^{−1}\\) из предыдущего упражнения, оцените \\(\beta_{y} \circ g\\) 
> для произвольного объекта y и произвольной стрелки \\(g : a \to y\\).

???

## Упражнение 4.1.1. 

> Составьте реализации трех других функций Bool -> Bool.

```dotty
enum Bool:
  case True, False

def alwaysTrue(b: Bool): Bool = Bool.True

def alwaysFalse(b: Bool): Bool = Bool.False

def same(b: Bool): Bool = b

def not(b: Bool): Bool =
  b match
    case Bool.True  => Bool.False
    case Bool.False => Bool.True
``` 

## Упражнение 4.4.1. 

> Реализуйте на Haskell две функции, образующие изоморфизм между Either + Void и a.

Реализация на Scala:

```dotty
final abstract class Void()

def f[A](either: Either[Void, A]): A =
  either match
    case Left(value) => ??? // imposible
    case Right(a)    => a

def fReverse[A](a: A): Either[Void, A] = Right(a)
```

## Упражнение 4.4.2. 

> Покажите, что определенная выше биекция естественна. 
> Подсказка: и f, и g, меняют фокус пост-композицией с \\(k : x \to y\\).

???

## Упражнение 4.4.3. 

> Реализуйте на Haskell функцию, свидетельствующую об изоморфизме между Either a b и Either b a. 
> Обратите внимание, что эта функция является обратной самой себе.

```dotty
def f[A, B](either: Either[A, B]): Either[B, A] =
  either match
    case Left(a)  => Right(a)
    case Right(b) => Left(b)
```

## Упражнение 4.4.4. 

> Покажите, что функториальность сохраняет композицию. 
> 
> Подсказка: возьмите две компонуемые стрелки, \\(g : b \to b'\\) и \\(g': b' → b''\\), 
> и покажите, что применение \\(g' \circ g\\) дает тот же результат, 
> что и первое применение \\(g\\) для преобразования \\(a + b\\) в \\(a + b'\\), 
> а затем применяя \\(g'\\) для преобразования \\(a + b'\\) к \\(a + b''\\).

Применение \\((g \circ g')\\) к \\(\textrm{Left(a)}\\) приводит к \\(\textrm{Left(a)}\\) в тип-сумме \\(a + b''\\).
Аналогично последовательное применение \\(g\\) и \\(g'\\) к \\(\textrm{Left(a)}\\) 
вначале приводит к \\(\textrm{Left(a)}\\) в тип-сумме \\(a + b'\\), 
затем - к \\(\textrm{Left(a)}\\) в тип-сумме \\(a + b''\\).

Применение \\((g \circ g')\\) к \\(\textrm{Right(b)}\\) приводит к \\(\textrm{Right(b'')}\\) в тип-сумме \\(a + b''\\).
Аналогично последовательное применение \\(g\\) и \\(g'\\) к \\(\textrm{Right(b)}\\)
вначале приводит к \\(\textrm{Right(b')}\\) в тип-сумме \\(a + b'\\), 
затем - к \\(\textrm{Right(b'')}\\) в тип-сумме \\(a + b''\\).

## Упражнение 4.4.5. 

> Покажите, что функториальность сохраняет тождественность. 
> Подсказка: используйте \\(id\_{b}\\) и покажите, что она отображается к \\(id\_{a+b}\\).

Если в качестве преобразования взять \\(f = id\_{a}, g = id\_{b}\\), то тогда пара стрелок
\\((Left \circ id\_{a}, Right \circ id\_{b})\\) будет отображать \\((a \to a, b \to b)\\),
т.е. будет определять тождественную стрелку \\(id\_{a+b}: (a \to a, b \to b)\\). 

## Упражнение 5.1.1. 

> Покажите, что биекция в доказательстве левой единицы естественна. 
> Подсказка: смените фокус с помощью стрелки \\(g : a \to b\\).

???

## Упражнение 5.1.2. 

> Постройте стрелку \\(h : b + a \times b \to (1 + a) \times b\\). Эта стрелка единственная? 
> Подсказка: это отображение-внутрь произведения, поэтому оно задается парой стрелок. 
> Эти стрелки, в свою очередь, отображаютвне сумму, каждая из которых задается, поэтому, парой стрелок. 
> Подсказка: отображение \\(b \to 1 + a\\) задается как \\((Left \circ !)\\)

???

## Упражнение 5.1.3. 

> Повторите предыдущее упражнение, рассматривая, на этот раз, h как отображение-вне суммы.

???

## Упражнение 5.1.4. 

> Реализуйте Haskell-функцию maybeAB :: Either b (a, b) -> (Maybe a, b). 
> Является ли эта функция однозначно определенной сигнатурой своего типа или есть некоторая свобода действий?

```dotty
def maybeAB[A, B](either: Either[B, (A, B)]): (Option[A], B) =
  either match
    case Left(b)       => (None, b)
    case Right((a, b)) => (Some(a), b)
```

Да, функция однозначно задается своей сигнатурой.

## Упражнение 6.3.1. 

> Покажите, что: \\(2 \times a \cong a + a\\), где 2 — логический тип. 
> Сначала проведите доказательство схематически, а затем реализуйте две Haskell-функции, свидетельствующие об изоморфизме.

```dotty
def toSum[A](product: (Boolean, A)): Either[A, A] =
  if product._1 then Left(product._2)
  else Right(product._2)

def toProduct[A](either: Either[A, A]): (Boolean, A) =
  either match
    case Left(a)  => (true, a)
    case Right(a) => (false, a)
```

## Упражнение 7.1.1. 

> Реализуйте каррированную версию сложения как отображение-вне N в функциональный объект \\(N^{N}\\) . 
> Подсказка: используйте следующие типы в рекурсоре:
> init :: Nat -> Nat
> step :: (Nat -> Nat) -> (Nat -> Nat)

```dotty
enum Nat:
  case Zero
  case Succ(n: Nat)

import Nat.*

val one = Succ(Zero)
val two = Succ(one)
val three = Succ(two)

def rec[A](init: A, step: A => A, n: Nat): A =
  n match
    case Zero    => init
    case Succ(m) => step(rec(init, step, m))

rec(two, Succ(_), three) // 5

val plusTwo: Nat => Nat = n => rec(two, Succ(_), n)
plusTwo(three) // 5

val curryInit: Nat => Nat = n => n
val curryStep: (Nat => Nat) => (Nat => Nat) = f => k => Succ(f(k))
val curry: Nat => Nat => Nat = n => rec[Nat => Nat](curryInit, curryStep, n)

curry(Zero)(two)  // 2
curry(three)(two) // 5
```

## Упражнение 7.2.1. 

> Подумайте, что произойдет, если заменить a в определении списка терминальным объектом. 
> Подсказка: что такое кодирование натуральных чисел по основанию один?

???

## Упражнение 7.2.2. 

> Сколько существует отображений \\(h : L\_{a} → 1 + a\\)? 
> Можно ли получить их все, используя рекурсор списка? 
> Что можно сказать насчет Haskell-функций сигнатуры: \\(h :: \[a\] -> Maybe a\\)

???

## Упражнение 7.2.3. 

> Реализуйте функцию, извлекающую третий элемент из списка, если список достаточно длинный. 
> Подсказка: используйте Maybe a для типа результата.

```dotty
def get[A](list: List[A], n: Int): Option[A] =
  list match
    case Nil => None
    case head :: next =>
      if n == 0 then Some(head)
      else get(next, n - 1)

get(List(1, 2, 3, 4, 5), 2)
// Some(3)
```

## Упражнение 8.2.1. 

> Опишите функтор, источником которого является категория «шагающая стрелка». 
> Это категория фигурок с двумя объектами и одной стрелкой между ними (плюс обязательные тождественные стрелки).

???

## Упражнение 8.2.2. 

> Категория «ходячий изо» аналогична категории «шагающая стрелка», плюс еще одна стрелка, идущая обратно от b к а. 
> Покажите, что функтор из этой категории всегда выбирает изоморфизм в целевой категории.

???

## Упражнение 8.3.1. 

> Покажите, что WithInt является функтором data WithInt a = WithInt a Int

???

## Упражнение 8.3.2. 

> Покажите, что Id есть Functor. Подсказка: реализуйте для него экземпляр Functor.

```dotty
trait Functor[F[_]]:
  extension [A](fa: F[A])
    def map[B](f: A => B): F[B]

case class Id[A](value: A)

given idFunctor: Functor[Id] with
  extension [A](as: Id[A]) 
    override def map[B](f: A => B): Id[B] = Id(f(as.value))
```

## Упражнение 8.3.3. 

> Покажите, что (Const c) есть Functor. 
> Подсказка: Конструктор типа принимает два аргумента, 
> но здесь он частично применяется к первому аргументу. 
> Он функториален по второму аргументу.

```dotty
trait Functor[F[_]]:
  extension [A](fa: F[A]) def map[B](f: A => B): F[B]

case class Const[C, A](c: C)

given constFunctor[C]: Functor[[X] =>> Const[C, X]] with
  extension [A](as: Const[C, A])
    override def map[B](f: A => B): Const[C, B] = Const[C, B](as.c)
```

## Упражнение 8.3.4. 

> Покажите, что MoreThanA является бифунктором. data MoreThanA a b = More a (Maybe b)

???

## Упражнение 8.5.1. 

> Определите композицию «Functor после Contravariant» 
> Подсказка: вы можете повторно использовать Compose, но указав объявление другого экземпляра.

???

## Упражнение 9.3.1. 

> Докажите условие естественности композиции естественных преобразований: 
> \\(\gamma\_{y} \circ \mathit{Ff} = \mathit{Hf} \circ \gamma\_{x}\\) 
> Подсказка: используйте определение \\(\gamma\\) и условия естественности для \\(\alpha\\) и \\(\beta\\).

???

## Упражнение 9.3.2. 

> Реализуйте две версии горизонтальной композиции safeHead после reverse. 
> Сравните их результаты, действующие на различные аргументы.

???

## Упражнение 9.3.3. 

> Сделайте то же самое с горизонтальной композицией reverse после safeHead.

???

---

**Ссылки:**

- The Dao of Functional Programming - Bartosz Milewski:
    - [Дао функционального программирования][Дао ФП]
    - [The Dao of Functional Programming](https://github.com/BartoszMilewski/Publications/blob/master/TheDaoOfFP/DaoFP.pdf)


[Дао ФП]: https://henrychern.wordpress.com/2022/09/23/milewski-%d0%b4%d0%b0%d0%be-%d1%84%d1%83%d0%bd%d0%ba%d1%86%d0%b8%d0%be%d0%bd%d0%b0%d0%bb%d1%8c%d0%bd%d0%be%d0%b3%d0%be-%d0%bf%d1%80%d0%be%d0%b3%d1%80%d0%b0%d0%bc%d0%bc%d0%b8%d1%80%d0%be%d0%b2%d0%b0/
